module BoolAlgebra

export BoolSymbol, And, Or, Not, @symbol, @symbols, simplify, substitude

import Base.|, Base.&, Base.!

abstract type BoolExpr end
AbstractBool = Union{BoolExpr, Bool}

struct BoolSymbol <: BoolExpr
    boolsym :: Symbol
end

Base.show(io::IO, p::BoolSymbol) = print(io, "$(p.boolsym)::BoolSymbol")

struct And <: BoolExpr
    left :: AbstractBool
    right :: AbstractBool
end

struct Or <: BoolExpr
    left :: AbstractBool
    right :: AbstractBool
end

struct Not <: BoolExpr
    boolsym :: AbstractBool
end

(|)(a::AbstractBool, b::AbstractBool) = Or(a, b)
(&)(a::AbstractBool, b::AbstractBool) = And(a, b)
(!)(a::AbstractBool) = Not(a)

macro symbol(ex)
    sym = BoolSymbol(ex)
    return esc(:($ex = $sym))
end

macro symbols(exs...)
    return esc(Expr(:(=), Expr(:tuple, exs...), Expr(:tuple, BoolSymbol.(exs)...)))
end


"""
    for_all_fields(node, f::Function)::Bool
# Argument
`node`: 当前节点
`f`: 检验函数 child → Bool
"""
function for_all_fields(node, f::Function)::Bool
    id(x) = x
    return mapreduce(id, &, [f(eval(:($node.$child))) for child in fieldnames(typeof(node))]; init = true)
end


"""
    walk_construct(node, f::Function)
深度优先遍历（fields）式构建
# Argument
`node`: 当前节点
`f`: 替换函数 node → node
"""
function walk_construct(node, f::Function)
    if fieldcount(typeof(node)) == 0
        return f(node)
    else
        # node_children_walked = eval(Expr(:call, :(typeof($node)), [eval(:(walk_construct($node.$child, $f))) for child in fieldnames(typeof(node))]...))
        node_children_walked = eval(Expr(:call, :(typeof($node)), [:(walk_construct($node.$child, $f)) for child in fieldnames(typeof(node))]...))
        if for_all_fields(node_children_walked, (child)->(fieldcount(typeof(child)) == 0))
            return f(node_children_walked)
        end
        return node_children_walked
    end
end

"""
    simplify(ex::AbstractBool)::AbstractBool
具体值化简
"""
function simplify(ex::AbstractBool)::AbstractBool
    sub_dict = Dict(And => :(&), Or => :(|), Not => :(!))
    function _sub(node, rules::Dict)
        if typeof(node) in keys(rules)
            return eval(Expr(:call, rules[typeof(node)], [eval(:($node.$child)) for child in fieldnames(typeof(node))]...))
        else
            return node
        end
    end
    return walk_construct(ex, node -> _sub(node, sub_dict))
end

"""
    substitude(ex::AbstractBool, rules::Dict{<:AbstractBool, <:AbstractBool})::AbstractBool
替换
"""
function substitude(ex::AbstractBool, rules::Dict{<:AbstractBool, <:AbstractBool})::AbstractBool
    function _sub(node, rules::Dict)
        if node in keys(rules)
            return rules[node]
        else
            return node
        end
    end
    return walk_construct(ex, node -> _sub(node, rules))
end


# function test()
#     @symbol p
#     simplify(Or(false, true))
# end

# test()

end